(set-logic QF_AUFLIA)
(set-info :source |
Unbounded version of the queue lock algorithm.


|)
(set-info :smt-lib-version 2.6)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x_0 () Int)
(declare-fun x_1 () Int)
(declare-fun x_2 () (Array Int Int))
(declare-fun x_3 () Int)
(declare-fun x_4 () Int)
(declare-fun x_5 () Bool)
(declare-fun x_6 () Int)
(declare-fun x_7 () (Array Int Int))
(declare-fun x_8 () Int)
(declare-fun x_9 () (Array Int Int))
(declare-fun x_10 () Int)
(declare-fun x_11 () Bool)
(declare-fun x_12 () Int)
(declare-fun x_13 () Int)
(declare-fun x_14 () Int)
(declare-fun x_15 () Int)
(declare-fun x_16 () Int)
(declare-fun x_17 () (Array Int Int))
(declare-fun x_18 () Int)
(declare-fun x_19 () Int)
(declare-fun x_20 () Int)
(declare-fun x_21 () Int)
(declare-fun x_22 () Int)
(declare-fun x_23 () (Array Int Int))
(declare-fun x_24 () Int)
(declare-fun x_25 () Bool)
(declare-fun x_26 () Int)
(declare-fun x_27 () Int)
(declare-fun x_28 () Int)
(declare-fun x_29 () Int)
(declare-fun x_30 () Int)
(declare-fun x_31 () (Array Int Int))
(declare-fun x_32 () Int)
(declare-fun x_33 () Int)
(declare-fun x_34 () Int)
(declare-fun x_35 () Int)
(declare-fun x_36 () Int)
(declare-fun x_37 () (Array Int Int))
(declare-fun x_38 () Int)
(declare-fun x_39 () Bool)
(declare-fun x_40 () Int)
(declare-fun x_41 () Int)
(declare-fun x_42 () Int)
(declare-fun x_43 () Int)
(declare-fun x_44 () Int)
(declare-fun x_45 () (Array Int Int))
(declare-fun x_46 () Int)
(declare-fun x_47 () Int)
(declare-fun x_48 () Int)
(declare-fun x_49 () Int)
(declare-fun x_50 () Int)
(declare-fun x_51 () (Array Int Int))
(declare-fun x_52 () Int)
(declare-fun x_53 () Bool)
(declare-fun x_54 () Int)
(declare-fun x_55 () Int)
(declare-fun x_56 () Int)
(declare-fun x_57 () Int)
(declare-fun x_58 () Int)
(declare-fun x_59 () (Array Int Int))
(declare-fun x_60 () Int)
(declare-fun x_61 () Int)
(declare-fun x_62 () Int)
(declare-fun x_63 () Int)
(declare-fun x_64 () Int)
(declare-fun x_65 () (Array Int Int))
(declare-fun x_66 () Int)
(declare-fun x_67 () Bool)
(declare-fun x_68 () Int)
(declare-fun x_69 () Int)
(declare-fun x_70 () Int)
(declare-fun x_71 () Int)
(declare-fun x_72 () Int)
(declare-fun x_73 () (Array Int Int))
(declare-fun x_74 () Int)
(declare-fun x_75 () Int)
(declare-fun x_76 () Int)
(declare-fun x_77 () Int)
(declare-fun x_78 () Int)
(declare-fun x_79 () (Array Int Int))
(declare-fun x_80 () Int)
(declare-fun x_81 () Bool)
(declare-fun x_82 () Int)
(declare-fun x_83 () Int)
(declare-fun x_84 () Int)
(declare-fun x_85 () Int)
(declare-fun x_86 () Int)
(declare-fun x_87 () (Array Int Int))
(declare-fun x_88 () Int)
(declare-fun x_89 () Int)
(declare-fun x_90 () Int)
(declare-fun x_91 () Int)
(declare-fun x_92 () Int)
(declare-fun x_93 () (Array Int Int))
(declare-fun x_94 () Int)
(declare-fun x_95 () Bool)
(declare-fun x_96 () Int)
(declare-fun x_97 () Int)
(declare-fun x_98 () Int)
(declare-fun x_99 () Int)
(declare-fun x_100 () Int)
(declare-fun x_101 () (Array Int Int))
(declare-fun x_102 () Int)
(declare-fun x_103 () Int)
(declare-fun x_104 () Int)
(declare-fun x_105 () Int)
(declare-fun x_106 () Int)
(declare-fun x_107 () (Array Int Int))
(declare-fun x_108 () Int)
(declare-fun x_109 () Bool)
(declare-fun x_110 () Int)
(declare-fun x_111 () Int)
(declare-fun x_112 () Int)
(declare-fun x_113 () Int)
(declare-fun x_114 () Int)
(declare-fun x_115 () (Array Int Int))
(declare-fun x_116 () Int)
(declare-fun x_117 () Int)
(declare-fun x_118 () Int)
(declare-fun x_119 () Int)
(declare-fun x_120 () Int)
(declare-fun x_121 () (Array Int Int))
(declare-fun x_122 () Int)
(declare-fun x_123 () Bool)
(declare-fun x_124 () Int)
(declare-fun x_125 () Int)
(declare-fun x_126 () Int)
(declare-fun x_127 () Int)
(declare-fun x_128 () Int)
(declare-fun x_129 () (Array Int Int))
(declare-fun x_130 () Int)
(declare-fun x_131 () Int)
(declare-fun x_132 () Int)
(declare-fun x_133 () Int)
(declare-fun x_134 () Int)
(declare-fun x_135 () (Array Int Int))
(declare-fun x_136 () Int)
(declare-fun x_137 () Bool)
(declare-fun x_138 () Int)
(declare-fun x_139 () Int)
(declare-fun x_140 () Int)
(declare-fun x_141 () Int)
(declare-fun x_142 () Int)
(declare-fun x_143 () (Array Int Int))
(declare-fun x_144 () Int)
(declare-fun x_145 () Int)
(declare-fun x_146 () Int)
(declare-fun x_147 () Int)
(declare-fun x_148 () Int)
(declare-fun x_149 () (Array Int Int))
(declare-fun x_150 () Int)
(declare-fun x_151 () Bool)
(declare-fun x_152 () Int)
(declare-fun x_153 () Int)
(declare-fun x_154 () Int)
(declare-fun x_155 () Int)
(declare-fun x_156 () Int)
(declare-fun x_157 () (Array Int Int))
(declare-fun x_158 () Int)
(declare-fun x_159 () Int)
(declare-fun x_160 () Int)
(declare-fun x_161 () Int)
(declare-fun x_162 () Int)
(declare-fun x_163 () (Array Int Int))
(declare-fun x_164 () Int)
(declare-fun x_165 () Bool)
(declare-fun x_166 () Int)
(declare-fun x_167 () Int)
(declare-fun x_168 () Int)
(declare-fun x_169 () Int)
(declare-fun x_170 () Int)
(declare-fun x_171 () (Array Int Int))
(declare-fun x_172 () Int)
(declare-fun x_173 () Int)
(declare-fun x_174 () Int)
(declare-fun x_175 () Int)
(declare-fun x_176 () Int)
(declare-fun x_177 () (Array Int Int))
(declare-fun x_178 () Int)
(declare-fun x_179 () Bool)
(declare-fun x_180 () Int)
(declare-fun x_181 () Int)
(declare-fun x_182 () Int)
(declare-fun x_183 () Int)
(declare-fun x_184 () Int)
(declare-fun x_185 () (Array Int Int))
(declare-fun x_186 () Int)
(declare-fun x_187 () Int)
(declare-fun x_188 () Int)
(declare-fun x_189 () Int)
(declare-fun x_190 () Int)
(declare-fun x_191 () (Array Int Int))
(declare-fun x_192 () Int)
(declare-fun x_193 () Bool)
(declare-fun x_194 () Int)
(declare-fun x_195 () Int)
(declare-fun x_196 () Int)
(declare-fun x_197 () Int)
(declare-fun x_198 () Int)
(declare-fun x_199 () (Array Int Int))
(declare-fun x_200 () Int)
(declare-fun x_201 () Int)
(declare-fun x_202 () Int)
(declare-fun x_203 () Int)
(declare-fun x_204 () Int)
(declare-fun x_205 () (Array Int Int))
(declare-fun x_206 () Int)
(declare-fun x_207 () Bool)
(declare-fun x_208 () Int)
(declare-fun x_209 () Int)
(declare-fun x_210 () Int)
(declare-fun x_211 () Int)
(declare-fun x_212 () Int)
(declare-fun x_213 () (Array Int Int))
(declare-fun x_214 () Int)
(declare-fun x_215 () Int)
(declare-fun x_216 () Int)
(declare-fun x_217 () Int)
(declare-fun x_218 () Int)
(declare-fun x_219 () (Array Int Int))
(declare-fun x_220 () Int)
(declare-fun x_221 () Bool)
(declare-fun x_222 () Int)
(declare-fun x_223 () Int)
(declare-fun x_224 () Int)
(declare-fun x_225 () Int)
(declare-fun x_226 () Int)
(declare-fun x_227 () (Array Int Int))
(declare-fun x_228 () Int)
(declare-fun x_229 () Int)
(declare-fun x_230 () Int)
(declare-fun x_231 () Int)
(declare-fun x_232 () Int)
(declare-fun x_233 () (Array Int Int))
(declare-fun x_234 () Int)
(declare-fun x_235 () Bool)
(declare-fun x_236 () Int)
(declare-fun x_237 () Int)
(declare-fun x_238 () Int)
(declare-fun x_239 () Int)
(declare-fun x_240 () Int)
(declare-fun x_241 () (Array Int Int))
(declare-fun x_242 () Int)
(declare-fun x_243 () Int)
(declare-fun x_244 () Int)
(declare-fun x_245 () Int)
(declare-fun x_246 () Int)
(declare-fun x_247 () (Array Int Int))
(declare-fun x_248 () Int)
(declare-fun x_249 () Bool)
(declare-fun x_250 () Int)
(declare-fun x_251 () Int)
(declare-fun x_252 () Int)
(declare-fun x_253 () Int)
(declare-fun x_254 () Int)
(declare-fun x_255 () (Array Int Int))
(declare-fun x_256 () Int)
(declare-fun x_257 () Int)
(declare-fun x_258 () Int)
(declare-fun x_259 () Int)
(declare-fun x_260 () Int)
(declare-fun x_261 () (Array Int Int))
(declare-fun x_262 () Int)
(declare-fun x_263 () Bool)
(declare-fun x_264 () Int)
(declare-fun x_265 () Int)
(declare-fun x_266 () Int)
(declare-fun x_267 () Int)
(declare-fun x_268 () Int)
(declare-fun x_269 () (Array Int Int))
(declare-fun x_270 () Int)
(declare-fun x_271 () Int)
(declare-fun x_272 () Int)
(declare-fun x_273 () Int)
(declare-fun x_274 () Int)
(declare-fun x_275 () (Array Int Int))
(declare-fun x_276 () Int)
(declare-fun x_277 () Bool)
(declare-fun x_278 () Int)
(declare-fun x_279 () Int)
(declare-fun x_280 () Int)
(declare-fun x_281 () Int)
(declare-fun x_282 () Int)
(declare-fun x_283 () (Array Int Int))
(declare-fun x_284 () Int)
(declare-fun x_285 () Int)
(declare-fun x_286 () Int)
(declare-fun x_287 () Int)
(declare-fun x_288 () Int)
(declare-fun x_289 () (Array Int Int))
(declare-fun x_290 () Int)
(declare-fun x_291 () Bool)
(declare-fun x_292 () Int)
(declare-fun x_293 () Int)
(declare-fun x_294 () Int)
(declare-fun x_295 () Int)
(declare-fun x_296 () Int)
(declare-fun x_297 () (Array Int Int))
(declare-fun x_298 () Int)
(declare-fun x_299 () Int)
(declare-fun x_300 () Int)
(declare-fun x_301 () Int)
(declare-fun x_302 () Int)
(declare-fun x_303 () (Array Int Int))
(declare-fun x_304 () Int)
(declare-fun x_305 () Bool)
(declare-fun x_306 () Int)
(declare-fun x_307 () Int)
(declare-fun x_308 () Int)
(declare-fun x_309 () Int)
(declare-fun x_310 () Int)
(declare-fun x_311 () (Array Int Int))
(declare-fun x_312 () Int)
(declare-fun x_313 () Int)
(declare-fun x_314 () Int)
(declare-fun x_315 () Int)
(declare-fun x_316 () Int)
(declare-fun x_317 () (Array Int Int))
(declare-fun x_318 () Int)
(declare-fun x_319 () Bool)
(declare-fun x_320 () Int)
(declare-fun x_321 () Int)
(declare-fun x_322 () Int)
(declare-fun x_323 () Int)
(declare-fun x_324 () Int)
(declare-fun x_325 () (Array Int Int))
(declare-fun x_326 () Int)
(declare-fun x_327 () Int)
(declare-fun x_328 () Int)
(declare-fun x_329 () Int)
(declare-fun x_330 () Int)
(declare-fun x_331 () (Array Int Int))
(declare-fun x_332 () Int)
(declare-fun x_333 () Bool)
(declare-fun x_334 () Int)
(declare-fun x_335 () Int)
(declare-fun x_336 () Int)
(declare-fun x_337 () Int)
(declare-fun x_338 () Int)
(declare-fun x_339 () (Array Int Int))
(declare-fun x_340 () Int)
(declare-fun x_341 () Int)
(declare-fun x_342 () Int)
(declare-fun x_343 () Int)
(declare-fun x_344 () Int)
(declare-fun x_345 () (Array Int Int))
(declare-fun x_346 () Int)
(declare-fun x_347 () Bool)
(declare-fun x_348 () Int)
(declare-fun x_349 () Int)
(declare-fun x_350 () Int)
(declare-fun x_351 () Int)
(declare-fun x_352 () Int)
(declare-fun x_353 () (Array Int Int))
(declare-fun x_354 () Int)
(declare-fun x_355 () Int)
(declare-fun x_356 () Int)
(declare-fun x_357 () Int)
(declare-fun x_358 () Int)
(declare-fun x_359 () Int)
(declare-fun x_360 () Int)
(declare-fun x_361 () Int)
(declare-fun x_362 () Int)
(declare-fun x_363 () Int)
(declare-fun x_364 () Int)
(declare-fun x_365 () Int)
(declare-fun x_366 () Int)
(declare-fun x_367 () Int)
(declare-fun x_368 () Int)
(declare-fun x_369 () Int)
(declare-fun x_370 () Int)
(declare-fun x_371 () Int)
(declare-fun x_372 () Int)
(declare-fun x_373 () Int)
(declare-fun x_374 () Int)
(declare-fun x_375 () Int)
(declare-fun x_376 () Int)
(declare-fun x_377 () Int)
(declare-fun x_378 () Int)
(declare-fun x_379 () Int)
(declare-fun x_380 () Int)
(declare-fun x_381 () Int)
(declare-fun x_382 () Int)
(declare-fun x_383 () Int)
(declare-fun x_384 () Int)
(declare-fun x_385 () Int)
(declare-fun x_386 () Int)
(declare-fun x_387 () Int)
(declare-fun x_388 () Int)
(declare-fun x_389 () Int)
(declare-fun x_390 () Int)
(declare-fun x_391 () Int)
(declare-fun x_392 () Int)
(declare-fun x_393 () Int)
(declare-fun x_394 () Int)
(declare-fun x_395 () Int)
(declare-fun x_396 () Int)
(declare-fun x_397 () Int)
(declare-fun x_398 () Int)
(declare-fun x_399 () Int)
(declare-fun x_400 () Int)
(declare-fun x_401 () Int)
(declare-fun x_402 () Int)
(declare-fun x_403 () Int)
(declare-fun x_404 () Int)
(declare-fun x_405 () Int)
(declare-fun x_406 () Int)
(declare-fun x_407 () Int)
(declare-fun x_408 () Int)
(declare-fun x_409 () Int)
(declare-fun x_410 () Int)
(declare-fun x_411 () Int)
(declare-fun x_412 () Int)
(declare-fun x_413 () Int)
(declare-fun x_414 () Int)
(declare-fun x_415 () Int)
(declare-fun x_416 () Int)
(declare-fun x_417 () Int)
(declare-fun x_418 () Int)
(declare-fun x_419 () Int)
(declare-fun x_420 () Int)
(declare-fun x_421 () Int)
(declare-fun x_422 () Int)
(declare-fun x_423 () Int)
(declare-fun x_424 () Int)
(declare-fun x_425 () Int)
(declare-fun x_426 () Int)
(declare-fun x_427 () Int)
(declare-fun x_428 () Int)
(declare-fun x_429 () Int)
(declare-fun x_430 () Int)
(declare-fun x_431 () Int)
(declare-fun x_432 () Int)
(declare-fun x_433 () Int)
(declare-fun x_434 () Int)
(declare-fun x_435 () Int)
(declare-fun x_436 () Int)
(declare-fun x_437 () Int)
(declare-fun x_438 () Int)
(declare-fun x_439 () Int)
(declare-fun x_440 () Int)
(declare-fun x_441 () Int)
(declare-fun x_442 () Int)
(declare-fun x_443 () Int)
(declare-fun x_444 () Int)
(declare-fun x_445 () Int)
(declare-fun x_446 () Int)
(declare-fun x_447 () Int)
(declare-fun x_448 () Int)
(declare-fun x_449 () Int)
(declare-fun x_450 () Int)
(declare-fun x_451 () Int)
(declare-fun x_452 () Int)
(declare-fun x_453 () Int)
(declare-fun x_454 () Int)
(declare-fun x_455 () Int)
(declare-fun x_456 () Int)
(declare-fun x_457 () Int)
(declare-fun x_458 () Int)
(declare-fun x_459 () Int)
(declare-fun x_460 () Int)
(declare-fun x_461 () Int)
(declare-fun x_462 () Int)
(declare-fun x_463 () Int)
(declare-fun x_464 () Int)
(declare-fun x_465 () Int)
(declare-fun x_466 () Int)
(declare-fun x_467 () Int)
(declare-fun x_468 () Int)
(declare-fun x_469 () Int)
(declare-fun x_470 () Int)
(declare-fun x_471 () Int)
(declare-fun x_472 () Int)
(declare-fun x_473 () Int)
(declare-fun x_474 () Int)
(declare-fun x_475 () Int)
(declare-fun x_476 () Int)
(declare-fun x_477 () Int)
(declare-fun x_478 () Int)
(declare-fun x_479 () Int)
(declare-fun x_480 () Int)
(declare-fun x_481 () Int)
(declare-fun x_482 () Int)
(declare-fun x_483 () Int)
(declare-fun x_484 () Int)
(declare-fun x_485 () Int)
(declare-fun x_486 () Int)
(declare-fun x_487 () Int)
(declare-fun x_488 () Int)
(declare-fun x_489 () Int)
(declare-fun x_490 () Int)
(declare-fun x_491 () Int)
(declare-fun x_492 () Int)
(declare-fun x_493 () Int)
(declare-fun x_494 () Int)
(declare-fun x_495 () Int)
(declare-fun x_496 () Int)
(declare-fun x_497 () Int)
(declare-fun x_498 () Int)
(declare-fun x_499 () Int)
(declare-fun x_500 () Int)
(declare-fun x_501 () Int)
(declare-fun x_502 () Int)
(declare-fun x_503 () Int)
(declare-fun x_504 () Int)
(declare-fun x_505 () Int)
(declare-fun x_506 () Int)
(declare-fun x_507 () Int)
(declare-fun x_508 () Int)
(declare-fun x_509 () Int)
(declare-fun x_510 () Int)
(declare-fun x_511 () Int)
(assert (let ((?v_123 (= x_9 x_7)) (?v_120 (= x_10 x_0)) (?v_121 (= x_11 x_5)) (?v_124 (= x_12 x_1)) (?v_122 (not (<= x_1 x_0))) (?v_118 (= x_23 x_9)) (?v_115 (= x_24 x_10)) (?v_116 (= x_25 x_11)) (?v_119 (= x_26 x_12)) (?v_117 (not (<= x_12 x_10))) (?v_113 (= x_37 x_23)) (?v_110 (= x_38 x_24)) (?v_111 (= x_39 x_25)) (?v_114 (= x_40 x_26)) (?v_112 (not (<= x_26 x_24))) (?v_108 (= x_51 x_37)) (?v_105 (= x_52 x_38)) (?v_106 (= x_53 x_39)) (?v_109 (= x_54 x_40)) (?v_107 (not (<= x_40 x_38))) (?v_103 (= x_65 x_51)) (?v_100 (= x_66 x_52)) (?v_101 (= x_67 x_53)) (?v_104 (= x_68 x_54)) (?v_102 (not (<= x_54 x_52))) (?v_98 (= x_79 x_65)) (?v_95 (= x_80 x_66)) (?v_96 (= x_81 x_67)) (?v_99 (= x_82 x_68)) (?v_97 (not (<= x_68 x_66))) (?v_93 (= x_93 x_79)) (?v_90 (= x_94 x_80)) (?v_91 (= x_95 x_81)) (?v_94 (= x_96 x_82)) (?v_92 (not (<= x_82 x_80))) (?v_88 (= x_107 x_93)) (?v_85 (= x_108 x_94)) (?v_86 (= x_109 x_95)) (?v_89 (= x_110 x_96)) (?v_87 (not (<= x_96 x_94))) (?v_83 (= x_121 x_107)) (?v_80 (= x_122 x_108)) (?v_81 (= x_123 x_109)) (?v_84 (= x_124 x_110)) (?v_82 (not (<= x_110 x_108))) (?v_78 (= x_135 x_121)) (?v_75 (= x_136 x_122)) (?v_76 (= x_137 x_123)) (?v_79 (= x_138 x_124)) (?v_77 (not (<= x_124 x_122))) (?v_73 (= x_149 x_135)) (?v_70 (= x_150 x_136)) (?v_71 (= x_151 x_137)) (?v_74 (= x_152 x_138)) (?v_72 (not (<= x_138 x_136))) (?v_68 (= x_163 x_149)) (?v_65 (= x_164 x_150)) (?v_66 (= x_165 x_151)) (?v_69 (= x_166 x_152)) (?v_67 (not (<= x_152 x_150))) (?v_63 (= x_177 x_163)) (?v_60 (= x_178 x_164)) (?v_61 (= x_179 x_165)) (?v_64 (= x_180 x_166)) (?v_62 (not (<= x_166 x_164))) (?v_58 (= x_191 x_177)) (?v_55 (= x_192 x_178)) (?v_56 (= x_193 x_179)) (?v_59 (= x_194 x_180)) (?v_57 (not (<= x_180 x_178))) (?v_53 (= x_205 x_191)) (?v_50 (= x_206 x_192)) (?v_51 (= x_207 x_193)) (?v_54 (= x_208 x_194)) (?v_52 (not (<= x_194 x_192))) (?v_48 (= x_219 x_205)) (?v_45 (= x_220 x_206)) (?v_46 (= x_221 x_207)) (?v_49 (= x_222 x_208)) (?v_47 (not (<= x_208 x_206))) (?v_43 (= x_233 x_219)) (?v_40 (= x_234 x_220)) (?v_41 (= x_235 x_221)) (?v_44 (= x_236 x_222)) (?v_42 (not (<= x_222 x_220))) (?v_38 (= x_247 x_233)) (?v_35 (= x_248 x_234)) (?v_36 (= x_249 x_235)) (?v_39 (= x_250 x_236)) (?v_37 (not (<= x_236 x_234))) (?v_33 (= x_261 x_247)) (?v_30 (= x_262 x_248)) (?v_31 (= x_263 x_249)) (?v_34 (= x_264 x_250)) (?v_32 (not (<= x_250 x_248))) (?v_28 (= x_275 x_261)) (?v_25 (= x_276 x_262)) (?v_26 (= x_277 x_263)) (?v_29 (= x_278 x_264)) (?v_27 (not (<= x_264 x_262))) (?v_23 (= x_289 x_275)) (?v_20 (= x_290 x_276)) (?v_21 (= x_291 x_277)) (?v_24 (= x_292 x_278)) (?v_22 (not (<= x_278 x_276))) (?v_18 (= x_303 x_289)) (?v_15 (= x_304 x_290)) (?v_16 (= x_305 x_291)) (?v_19 (= x_306 x_292)) (?v_17 (not (<= x_292 x_290))) (?v_13 (= x_317 x_303)) (?v_10 (= x_318 x_304)) (?v_11 (= x_319 x_305)) (?v_14 (= x_320 x_306)) (?v_12 (not (<= x_306 x_304))) (?v_8 (= x_331 x_317)) (?v_5 (= x_332 x_318)) (?v_6 (= x_333 x_319)) (?v_9 (= x_334 x_320)) (?v_7 (not (<= x_320 x_318))) (?v_3 (= x_345 x_331)) (?v_0 (= x_346 x_332)) (?v_1 (= x_347 x_333)) (?v_4 (= x_348 x_334)) (?v_2 (not (<= x_334 x_332))) (?v_125 (select x_2 x_3)) (?v_126 (select x_2 x_4))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= x_4 x_3)) (= x_0 0)) (= x_1 0)) (= x_358 ?v_125)) (= x_358 1)) (= x_359 ?v_126)) (= x_359 1)) x_5) (= x_6 0)) (= x_360 (select x_7 x_0))) (= x_8 x_360)) (= x_361 (select x_9 x_10))) (= x_22 x_361)) (= x_362 (select x_23 x_24))) (= x_36 x_362)) (= x_363 (select x_37 x_38))) (= x_50 x_363)) (= x_364 (select x_51 x_52))) (= x_64 x_364)) (= x_365 (select x_65 x_66))) (= x_78 x_365)) (= x_366 (select x_79 x_80))) (= x_92 x_366)) (= x_367 (select x_93 x_94))) (= x_106 x_367)) (= x_368 (select x_107 x_108))) (= x_120 x_368)) (= x_369 (select x_121 x_122))) (= x_134 x_369)) (= x_370 (select x_135 x_136))) (= x_148 x_370)) (= x_371 (select x_149 x_150))) (= x_162 x_371)) (= x_372 (select x_163 x_164))) (= x_176 x_372)) (= x_373 (select x_177 x_178))) (= x_190 x_373)) (= x_374 (select x_191 x_192))) (= x_204 x_374)) (= x_375 (select x_205 x_206))) (= x_218 x_375)) (= x_376 (select x_219 x_220))) (= x_232 x_376)) (= x_377 (select x_233 x_234))) (= x_246 x_377)) (= x_378 (select x_247 x_248))) (= x_260 x_378)) (= x_379 (select x_261 x_262))) (= x_274 x_379)) (= x_380 (select x_275 x_276))) (= x_288 x_380)) (= x_381 (select x_289 x_290))) (= x_302 x_381)) (= x_382 (select x_303 x_304))) (= x_316 x_382)) (= x_383 (select x_317 x_318))) (= x_330 x_383)) (= x_384 (select x_331 x_332))) (= x_344 x_384)) (= x_349 (+ x_335 1))) (= x_385 (select x_339 x_351))) (= x_386 (select x_339 x_354))) (= x_387 (select x_339 x_356))) (or (or (or (and (and (and (and (and (and (and (= x_350 0) (= x_348 (+ x_334 1))) ?v_0) ?v_1) (= x_352 x_351)) (= x_385 1)) (= x_353 (store x_339 x_351 2))) (= x_345 (store x_331 x_334 x_351))) (and (and (and (and (and (and (and (and (and (= x_350 1) ?v_2) ?v_0) ?v_1) ?v_3) ?v_4) (= x_355 x_354)) (= x_386 2)) (= x_344 x_354)) (= x_353 (store x_339 x_354 3)))) (and (and (and (and (and (and (and (and (and (= x_350 2) ?v_2) (= x_346 (+ x_332 1))) ?v_1) ?v_3) ?v_4) (= x_357 x_356)) (= x_387 3)) (or (not (<= x_335 12)) (= x_344 x_356))) (= x_353 (store x_339 x_356 1)))) (and (and (and (and (and (= x_350 3) ?v_3) ?v_0) ?v_1) (= x_353 x_339)) ?v_4))) (= x_335 (+ x_321 1))) (= x_388 (select x_325 x_337))) (= x_389 (select x_325 x_340))) (= x_390 (select x_325 x_342))) (or (or (or (and (and (and (and (and (and (and (= x_336 0) (= x_334 (+ x_320 1))) ?v_5) ?v_6) (= x_338 x_337)) (= x_388 1)) (= x_339 (store x_325 x_337 2))) (= x_331 (store x_317 x_320 x_337))) (and (and (and (and (and (and (and (and (and (= x_336 1) ?v_7) ?v_5) ?v_6) ?v_8) ?v_9) (= x_341 x_340)) (= x_389 2)) (= x_330 x_340)) (= x_339 (store x_325 x_340 3)))) (and (and (and (and (and (and (and (and (and (= x_336 2) ?v_7) (= x_332 (+ x_318 1))) ?v_6) ?v_8) ?v_9) (= x_343 x_342)) (= x_390 3)) (or (not (<= x_321 12)) (= x_330 x_342))) (= x_339 (store x_325 x_342 1)))) (and (and (and (and (and (= x_336 3) ?v_8) ?v_5) ?v_6) (= x_339 x_325)) ?v_9))) (= x_321 (+ x_307 1))) (= x_391 (select x_311 x_323))) (= x_392 (select x_311 x_326))) (= x_393 (select x_311 x_328))) (or (or (or (and (and (and (and (and (and (and (= x_322 0) (= x_320 (+ x_306 1))) ?v_10) ?v_11) (= x_324 x_323)) (= x_391 1)) (= x_325 (store x_311 x_323 2))) (= x_317 (store x_303 x_306 x_323))) (and (and (and (and (and (and (and (and (and (= x_322 1) ?v_12) ?v_10) ?v_11) ?v_13) ?v_14) (= x_327 x_326)) (= x_392 2)) (= x_316 x_326)) (= x_325 (store x_311 x_326 3)))) (and (and (and (and (and (and (and (and (and (= x_322 2) ?v_12) (= x_318 (+ x_304 1))) ?v_11) ?v_13) ?v_14) (= x_329 x_328)) (= x_393 3)) (or (not (<= x_307 12)) (= x_316 x_328))) (= x_325 (store x_311 x_328 1)))) (and (and (and (and (and (= x_322 3) ?v_13) ?v_10) ?v_11) (= x_325 x_311)) ?v_14))) (= x_307 (+ x_293 1))) (= x_394 (select x_297 x_309))) (= x_395 (select x_297 x_312))) (= x_396 (select x_297 x_314))) (or (or (or (and (and (and (and (and (and (and (= x_308 0) (= x_306 (+ x_292 1))) ?v_15) ?v_16) (= x_310 x_309)) (= x_394 1)) (= x_311 (store x_297 x_309 2))) (= x_303 (store x_289 x_292 x_309))) (and (and (and (and (and (and (and (and (and (= x_308 1) ?v_17) ?v_15) ?v_16) ?v_18) ?v_19) (= x_313 x_312)) (= x_395 2)) (= x_302 x_312)) (= x_311 (store x_297 x_312 3)))) (and (and (and (and (and (and (and (and (and (= x_308 2) ?v_17) (= x_304 (+ x_290 1))) ?v_16) ?v_18) ?v_19) (= x_315 x_314)) (= x_396 3)) (or (not (<= x_293 12)) (= x_302 x_314))) (= x_311 (store x_297 x_314 1)))) (and (and (and (and (and (= x_308 3) ?v_18) ?v_15) ?v_16) (= x_311 x_297)) ?v_19))) (= x_293 (+ x_279 1))) (= x_397 (select x_283 x_295))) (= x_398 (select x_283 x_298))) (= x_399 (select x_283 x_300))) (or (or (or (and (and (and (and (and (and (and (= x_294 0) (= x_292 (+ x_278 1))) ?v_20) ?v_21) (= x_296 x_295)) (= x_397 1)) (= x_297 (store x_283 x_295 2))) (= x_289 (store x_275 x_278 x_295))) (and (and (and (and (and (and (and (and (and (= x_294 1) ?v_22) ?v_20) ?v_21) ?v_23) ?v_24) (= x_299 x_298)) (= x_398 2)) (= x_288 x_298)) (= x_297 (store x_283 x_298 3)))) (and (and (and (and (and (and (and (and (and (= x_294 2) ?v_22) (= x_290 (+ x_276 1))) ?v_21) ?v_23) ?v_24) (= x_301 x_300)) (= x_399 3)) (or (not (<= x_279 12)) (= x_288 x_300))) (= x_297 (store x_283 x_300 1)))) (and (and (and (and (and (= x_294 3) ?v_23) ?v_20) ?v_21) (= x_297 x_283)) ?v_24))) (= x_279 (+ x_265 1))) (= x_400 (select x_269 x_281))) (= x_401 (select x_269 x_284))) (= x_402 (select x_269 x_286))) (or (or (or (and (and (and (and (and (and (and (= x_280 0) (= x_278 (+ x_264 1))) ?v_25) ?v_26) (= x_282 x_281)) (= x_400 1)) (= x_283 (store x_269 x_281 2))) (= x_275 (store x_261 x_264 x_281))) (and (and (and (and (and (and (and (and (and (= x_280 1) ?v_27) ?v_25) ?v_26) ?v_28) ?v_29) (= x_285 x_284)) (= x_401 2)) (= x_274 x_284)) (= x_283 (store x_269 x_284 3)))) (and (and (and (and (and (and (and (and (and (= x_280 2) ?v_27) (= x_276 (+ x_262 1))) ?v_26) ?v_28) ?v_29) (= x_287 x_286)) (= x_402 3)) (or (not (<= x_265 12)) (= x_274 x_286))) (= x_283 (store x_269 x_286 1)))) (and (and (and (and (and (= x_280 3) ?v_28) ?v_25) ?v_26) (= x_283 x_269)) ?v_29))) (= x_265 (+ x_251 1))) (= x_403 (select x_255 x_267))) (= x_404 (select x_255 x_270))) (= x_405 (select x_255 x_272))) (or (or (or (and (and (and (and (and (and (and (= x_266 0) (= x_264 (+ x_250 1))) ?v_30) ?v_31) (= x_268 x_267)) (= x_403 1)) (= x_269 (store x_255 x_267 2))) (= x_261 (store x_247 x_250 x_267))) (and (and (and (and (and (and (and (and (and (= x_266 1) ?v_32) ?v_30) ?v_31) ?v_33) ?v_34) (= x_271 x_270)) (= x_404 2)) (= x_260 x_270)) (= x_269 (store x_255 x_270 3)))) (and (and (and (and (and (and (and (and (and (= x_266 2) ?v_32) (= x_262 (+ x_248 1))) ?v_31) ?v_33) ?v_34) (= x_273 x_272)) (= x_405 3)) (or (not (<= x_251 12)) (= x_260 x_272))) (= x_269 (store x_255 x_272 1)))) (and (and (and (and (and (= x_266 3) ?v_33) ?v_30) ?v_31) (= x_269 x_255)) ?v_34))) (= x_251 (+ x_237 1))) (= x_406 (select x_241 x_253))) (= x_407 (select x_241 x_256))) (= x_408 (select x_241 x_258))) (or (or (or (and (and (and (and (and (and (and (= x_252 0) (= x_250 (+ x_236 1))) ?v_35) ?v_36) (= x_254 x_253)) (= x_406 1)) (= x_255 (store x_241 x_253 2))) (= x_247 (store x_233 x_236 x_253))) (and (and (and (and (and (and (and (and (and (= x_252 1) ?v_37) ?v_35) ?v_36) ?v_38) ?v_39) (= x_257 x_256)) (= x_407 2)) (= x_246 x_256)) (= x_255 (store x_241 x_256 3)))) (and (and (and (and (and (and (and (and (and (= x_252 2) ?v_37) (= x_248 (+ x_234 1))) ?v_36) ?v_38) ?v_39) (= x_259 x_258)) (= x_408 3)) (or (not (<= x_237 12)) (= x_246 x_258))) (= x_255 (store x_241 x_258 1)))) (and (and (and (and (and (= x_252 3) ?v_38) ?v_35) ?v_36) (= x_255 x_241)) ?v_39))) (= x_237 (+ x_223 1))) (= x_409 (select x_227 x_239))) (= x_410 (select x_227 x_242))) (= x_411 (select x_227 x_244))) (or (or (or (and (and (and (and (and (and (and (= x_238 0) (= x_236 (+ x_222 1))) ?v_40) ?v_41) (= x_240 x_239)) (= x_409 1)) (= x_241 (store x_227 x_239 2))) (= x_233 (store x_219 x_222 x_239))) (and (and (and (and (and (and (and (and (and (= x_238 1) ?v_42) ?v_40) ?v_41) ?v_43) ?v_44) (= x_243 x_242)) (= x_410 2)) (= x_232 x_242)) (= x_241 (store x_227 x_242 3)))) (and (and (and (and (and (and (and (and (and (= x_238 2) ?v_42) (= x_234 (+ x_220 1))) ?v_41) ?v_43) ?v_44) (= x_245 x_244)) (= x_411 3)) (or (not (<= x_223 12)) (= x_232 x_244))) (= x_241 (store x_227 x_244 1)))) (and (and (and (and (and (= x_238 3) ?v_43) ?v_40) ?v_41) (= x_241 x_227)) ?v_44))) (= x_223 (+ x_209 1))) (= x_412 (select x_213 x_225))) (= x_413 (select x_213 x_228))) (= x_414 (select x_213 x_230))) (or (or (or (and (and (and (and (and (and (and (= x_224 0) (= x_222 (+ x_208 1))) ?v_45) ?v_46) (= x_226 x_225)) (= x_412 1)) (= x_227 (store x_213 x_225 2))) (= x_219 (store x_205 x_208 x_225))) (and (and (and (and (and (and (and (and (and (= x_224 1) ?v_47) ?v_45) ?v_46) ?v_48) ?v_49) (= x_229 x_228)) (= x_413 2)) (= x_218 x_228)) (= x_227 (store x_213 x_228 3)))) (and (and (and (and (and (and (and (and (and (= x_224 2) ?v_47) (= x_220 (+ x_206 1))) ?v_46) ?v_48) ?v_49) (= x_231 x_230)) (= x_414 3)) (or (not (<= x_209 12)) (= x_218 x_230))) (= x_227 (store x_213 x_230 1)))) (and (and (and (and (and (= x_224 3) ?v_48) ?v_45) ?v_46) (= x_227 x_213)) ?v_49))) (= x_209 (+ x_195 1))) (= x_415 (select x_199 x_211))) (= x_416 (select x_199 x_214))) (= x_417 (select x_199 x_216))) (or (or (or (and (and (and (and (and (and (and (= x_210 0) (= x_208 (+ x_194 1))) ?v_50) ?v_51) (= x_212 x_211)) (= x_415 1)) (= x_213 (store x_199 x_211 2))) (= x_205 (store x_191 x_194 x_211))) (and (and (and (and (and (and (and (and (and (= x_210 1) ?v_52) ?v_50) ?v_51) ?v_53) ?v_54) (= x_215 x_214)) (= x_416 2)) (= x_204 x_214)) (= x_213 (store x_199 x_214 3)))) (and (and (and (and (and (and (and (and (and (= x_210 2) ?v_52) (= x_206 (+ x_192 1))) ?v_51) ?v_53) ?v_54) (= x_217 x_216)) (= x_417 3)) (or (not (<= x_195 12)) (= x_204 x_216))) (= x_213 (store x_199 x_216 1)))) (and (and (and (and (and (= x_210 3) ?v_53) ?v_50) ?v_51) (= x_213 x_199)) ?v_54))) (= x_195 (+ x_181 1))) (= x_418 (select x_185 x_197))) (= x_419 (select x_185 x_200))) (= x_420 (select x_185 x_202))) (or (or (or (and (and (and (and (and (and (and (= x_196 0) (= x_194 (+ x_180 1))) ?v_55) ?v_56) (= x_198 x_197)) (= x_418 1)) (= x_199 (store x_185 x_197 2))) (= x_191 (store x_177 x_180 x_197))) (and (and (and (and (and (and (and (and (and (= x_196 1) ?v_57) ?v_55) ?v_56) ?v_58) ?v_59) (= x_201 x_200)) (= x_419 2)) (= x_190 x_200)) (= x_199 (store x_185 x_200 3)))) (and (and (and (and (and (and (and (and (and (= x_196 2) ?v_57) (= x_192 (+ x_178 1))) ?v_56) ?v_58) ?v_59) (= x_203 x_202)) (= x_420 3)) (or (not (<= x_181 12)) (= x_190 x_202))) (= x_199 (store x_185 x_202 1)))) (and (and (and (and (and (= x_196 3) ?v_58) ?v_55) ?v_56) (= x_199 x_185)) ?v_59))) (= x_181 (+ x_167 1))) (= x_421 (select x_171 x_183))) (= x_422 (select x_171 x_186))) (= x_423 (select x_171 x_188))) (or (or (or (and (and (and (and (and (and (and (= x_182 0) (= x_180 (+ x_166 1))) ?v_60) ?v_61) (= x_184 x_183)) (= x_421 1)) (= x_185 (store x_171 x_183 2))) (= x_177 (store x_163 x_166 x_183))) (and (and (and (and (and (and (and (and (and (= x_182 1) ?v_62) ?v_60) ?v_61) ?v_63) ?v_64) (= x_187 x_186)) (= x_422 2)) (= x_176 x_186)) (= x_185 (store x_171 x_186 3)))) (and (and (and (and (and (and (and (and (and (= x_182 2) ?v_62) (= x_178 (+ x_164 1))) ?v_61) ?v_63) ?v_64) (= x_189 x_188)) (= x_423 3)) (or (not (<= x_167 12)) (= x_176 x_188))) (= x_185 (store x_171 x_188 1)))) (and (and (and (and (and (= x_182 3) ?v_63) ?v_60) ?v_61) (= x_185 x_171)) ?v_64))) (= x_167 (+ x_153 1))) (= x_424 (select x_157 x_169))) (= x_425 (select x_157 x_172))) (= x_426 (select x_157 x_174))) (or (or (or (and (and (and (and (and (and (and (= x_168 0) (= x_166 (+ x_152 1))) ?v_65) ?v_66) (= x_170 x_169)) (= x_424 1)) (= x_171 (store x_157 x_169 2))) (= x_163 (store x_149 x_152 x_169))) (and (and (and (and (and (and (and (and (and (= x_168 1) ?v_67) ?v_65) ?v_66) ?v_68) ?v_69) (= x_173 x_172)) (= x_425 2)) (= x_162 x_172)) (= x_171 (store x_157 x_172 3)))) (and (and (and (and (and (and (and (and (and (= x_168 2) ?v_67) (= x_164 (+ x_150 1))) ?v_66) ?v_68) ?v_69) (= x_175 x_174)) (= x_426 3)) (or (not (<= x_153 12)) (= x_162 x_174))) (= x_171 (store x_157 x_174 1)))) (and (and (and (and (and (= x_168 3) ?v_68) ?v_65) ?v_66) (= x_171 x_157)) ?v_69))) (= x_153 (+ x_139 1))) (= x_427 (select x_143 x_155))) (= x_428 (select x_143 x_158))) (= x_429 (select x_143 x_160))) (or (or (or (and (and (and (and (and (and (and (= x_154 0) (= x_152 (+ x_138 1))) ?v_70) ?v_71) (= x_156 x_155)) (= x_427 1)) (= x_157 (store x_143 x_155 2))) (= x_149 (store x_135 x_138 x_155))) (and (and (and (and (and (and (and (and (and (= x_154 1) ?v_72) ?v_70) ?v_71) ?v_73) ?v_74) (= x_159 x_158)) (= x_428 2)) (= x_148 x_158)) (= x_157 (store x_143 x_158 3)))) (and (and (and (and (and (and (and (and (and (= x_154 2) ?v_72) (= x_150 (+ x_136 1))) ?v_71) ?v_73) ?v_74) (= x_161 x_160)) (= x_429 3)) (or (not (<= x_139 12)) (= x_148 x_160))) (= x_157 (store x_143 x_160 1)))) (and (and (and (and (and (= x_154 3) ?v_73) ?v_70) ?v_71) (= x_157 x_143)) ?v_74))) (= x_139 (+ x_125 1))) (= x_430 (select x_129 x_141))) (= x_431 (select x_129 x_144))) (= x_432 (select x_129 x_146))) (or (or (or (and (and (and (and (and (and (and (= x_140 0) (= x_138 (+ x_124 1))) ?v_75) ?v_76) (= x_142 x_141)) (= x_430 1)) (= x_143 (store x_129 x_141 2))) (= x_135 (store x_121 x_124 x_141))) (and (and (and (and (and (and (and (and (and (= x_140 1) ?v_77) ?v_75) ?v_76) ?v_78) ?v_79) (= x_145 x_144)) (= x_431 2)) (= x_134 x_144)) (= x_143 (store x_129 x_144 3)))) (and (and (and (and (and (and (and (and (and (= x_140 2) ?v_77) (= x_136 (+ x_122 1))) ?v_76) ?v_78) ?v_79) (= x_147 x_146)) (= x_432 3)) (or (not (<= x_125 12)) (= x_134 x_146))) (= x_143 (store x_129 x_146 1)))) (and (and (and (and (and (= x_140 3) ?v_78) ?v_75) ?v_76) (= x_143 x_129)) ?v_79))) (= x_125 (+ x_111 1))) (= x_433 (select x_115 x_127))) (= x_434 (select x_115 x_130))) (= x_435 (select x_115 x_132))) (or (or (or (and (and (and (and (and (and (and (= x_126 0) (= x_124 (+ x_110 1))) ?v_80) ?v_81) (= x_128 x_127)) (= x_433 1)) (= x_129 (store x_115 x_127 2))) (= x_121 (store x_107 x_110 x_127))) (and (and (and (and (and (and (and (and (and (= x_126 1) ?v_82) ?v_80) ?v_81) ?v_83) ?v_84) (= x_131 x_130)) (= x_434 2)) (= x_120 x_130)) (= x_129 (store x_115 x_130 3)))) (and (and (and (and (and (and (and (and (and (= x_126 2) ?v_82) (= x_122 (+ x_108 1))) ?v_81) ?v_83) ?v_84) (= x_133 x_132)) (= x_435 3)) (or (not (<= x_111 12)) (= x_120 x_132))) (= x_129 (store x_115 x_132 1)))) (and (and (and (and (and (= x_126 3) ?v_83) ?v_80) ?v_81) (= x_129 x_115)) ?v_84))) (= x_111 (+ x_97 1))) (= x_436 (select x_101 x_113))) (= x_437 (select x_101 x_116))) (= x_438 (select x_101 x_118))) (or (or (or (and (and (and (and (and (and (and (= x_112 0) (= x_110 (+ x_96 1))) ?v_85) ?v_86) (= x_114 x_113)) (= x_436 1)) (= x_115 (store x_101 x_113 2))) (= x_107 (store x_93 x_96 x_113))) (and (and (and (and (and (and (and (and (and (= x_112 1) ?v_87) ?v_85) ?v_86) ?v_88) ?v_89) (= x_117 x_116)) (= x_437 2)) (= x_106 x_116)) (= x_115 (store x_101 x_116 3)))) (and (and (and (and (and (and (and (and (and (= x_112 2) ?v_87) (= x_108 (+ x_94 1))) ?v_86) ?v_88) ?v_89) (= x_119 x_118)) (= x_438 3)) (or (not (<= x_97 12)) (= x_106 x_118))) (= x_115 (store x_101 x_118 1)))) (and (and (and (and (and (= x_112 3) ?v_88) ?v_85) ?v_86) (= x_115 x_101)) ?v_89))) (= x_97 (+ x_83 1))) (= x_439 (select x_87 x_99))) (= x_440 (select x_87 x_102))) (= x_441 (select x_87 x_104))) (or (or (or (and (and (and (and (and (and (and (= x_98 0) (= x_96 (+ x_82 1))) ?v_90) ?v_91) (= x_100 x_99)) (= x_439 1)) (= x_101 (store x_87 x_99 2))) (= x_93 (store x_79 x_82 x_99))) (and (and (and (and (and (and (and (and (and (= x_98 1) ?v_92) ?v_90) ?v_91) ?v_93) ?v_94) (= x_103 x_102)) (= x_440 2)) (= x_92 x_102)) (= x_101 (store x_87 x_102 3)))) (and (and (and (and (and (and (and (and (and (= x_98 2) ?v_92) (= x_94 (+ x_80 1))) ?v_91) ?v_93) ?v_94) (= x_105 x_104)) (= x_441 3)) (or (not (<= x_83 12)) (= x_92 x_104))) (= x_101 (store x_87 x_104 1)))) (and (and (and (and (and (= x_98 3) ?v_93) ?v_90) ?v_91) (= x_101 x_87)) ?v_94))) (= x_83 (+ x_69 1))) (= x_442 (select x_73 x_85))) (= x_443 (select x_73 x_88))) (= x_444 (select x_73 x_90))) (or (or (or (and (and (and (and (and (and (and (= x_84 0) (= x_82 (+ x_68 1))) ?v_95) ?v_96) (= x_86 x_85)) (= x_442 1)) (= x_87 (store x_73 x_85 2))) (= x_79 (store x_65 x_68 x_85))) (and (and (and (and (and (and (and (and (and (= x_84 1) ?v_97) ?v_95) ?v_96) ?v_98) ?v_99) (= x_89 x_88)) (= x_443 2)) (= x_78 x_88)) (= x_87 (store x_73 x_88 3)))) (and (and (and (and (and (and (and (and (and (= x_84 2) ?v_97) (= x_80 (+ x_66 1))) ?v_96) ?v_98) ?v_99) (= x_91 x_90)) (= x_444 3)) (or (not (<= x_69 12)) (= x_78 x_90))) (= x_87 (store x_73 x_90 1)))) (and (and (and (and (and (= x_84 3) ?v_98) ?v_95) ?v_96) (= x_87 x_73)) ?v_99))) (= x_69 (+ x_55 1))) (= x_445 (select x_59 x_71))) (= x_446 (select x_59 x_74))) (= x_447 (select x_59 x_76))) (or (or (or (and (and (and (and (and (and (and (= x_70 0) (= x_68 (+ x_54 1))) ?v_100) ?v_101) (= x_72 x_71)) (= x_445 1)) (= x_73 (store x_59 x_71 2))) (= x_65 (store x_51 x_54 x_71))) (and (and (and (and (and (and (and (and (and (= x_70 1) ?v_102) ?v_100) ?v_101) ?v_103) ?v_104) (= x_75 x_74)) (= x_446 2)) (= x_64 x_74)) (= x_73 (store x_59 x_74 3)))) (and (and (and (and (and (and (and (and (and (= x_70 2) ?v_102) (= x_66 (+ x_52 1))) ?v_101) ?v_103) ?v_104) (= x_77 x_76)) (= x_447 3)) (or (not (<= x_55 12)) (= x_64 x_76))) (= x_73 (store x_59 x_76 1)))) (and (and (and (and (and (= x_70 3) ?v_103) ?v_100) ?v_101) (= x_73 x_59)) ?v_104))) (= x_55 (+ x_41 1))) (= x_448 (select x_45 x_57))) (= x_449 (select x_45 x_60))) (= x_450 (select x_45 x_62))) (or (or (or (and (and (and (and (and (and (and (= x_56 0) (= x_54 (+ x_40 1))) ?v_105) ?v_106) (= x_58 x_57)) (= x_448 1)) (= x_59 (store x_45 x_57 2))) (= x_51 (store x_37 x_40 x_57))) (and (and (and (and (and (and (and (and (and (= x_56 1) ?v_107) ?v_105) ?v_106) ?v_108) ?v_109) (= x_61 x_60)) (= x_449 2)) (= x_50 x_60)) (= x_59 (store x_45 x_60 3)))) (and (and (and (and (and (and (and (and (and (= x_56 2) ?v_107) (= x_52 (+ x_38 1))) ?v_106) ?v_108) ?v_109) (= x_63 x_62)) (= x_450 3)) (or (not (<= x_41 12)) (= x_50 x_62))) (= x_59 (store x_45 x_62 1)))) (and (and (and (and (and (= x_56 3) ?v_108) ?v_105) ?v_106) (= x_59 x_45)) ?v_109))) (= x_41 (+ x_27 1))) (= x_451 (select x_31 x_43))) (= x_452 (select x_31 x_46))) (= x_453 (select x_31 x_48))) (or (or (or (and (and (and (and (and (and (and (= x_42 0) (= x_40 (+ x_26 1))) ?v_110) ?v_111) (= x_44 x_43)) (= x_451 1)) (= x_45 (store x_31 x_43 2))) (= x_37 (store x_23 x_26 x_43))) (and (and (and (and (and (and (and (and (and (= x_42 1) ?v_112) ?v_110) ?v_111) ?v_113) ?v_114) (= x_47 x_46)) (= x_452 2)) (= x_36 x_46)) (= x_45 (store x_31 x_46 3)))) (and (and (and (and (and (and (and (and (and (= x_42 2) ?v_112) (= x_38 (+ x_24 1))) ?v_111) ?v_113) ?v_114) (= x_49 x_48)) (= x_453 3)) (or (not (<= x_27 12)) (= x_36 x_48))) (= x_45 (store x_31 x_48 1)))) (and (and (and (and (and (= x_42 3) ?v_113) ?v_110) ?v_111) (= x_45 x_31)) ?v_114))) (= x_27 (+ x_13 1))) (= x_454 (select x_17 x_29))) (= x_455 (select x_17 x_32))) (= x_456 (select x_17 x_34))) (or (or (or (and (and (and (and (and (and (and (= x_28 0) (= x_26 (+ x_12 1))) ?v_115) ?v_116) (= x_30 x_29)) (= x_454 1)) (= x_31 (store x_17 x_29 2))) (= x_23 (store x_9 x_12 x_29))) (and (and (and (and (and (and (and (and (and (= x_28 1) ?v_117) ?v_115) ?v_116) ?v_118) ?v_119) (= x_33 x_32)) (= x_455 2)) (= x_22 x_32)) (= x_31 (store x_17 x_32 3)))) (and (and (and (and (and (and (and (and (and (= x_28 2) ?v_117) (= x_24 (+ x_10 1))) ?v_116) ?v_118) ?v_119) (= x_35 x_34)) (= x_456 3)) (or (not (<= x_13 12)) (= x_22 x_34))) (= x_31 (store x_17 x_34 1)))) (and (and (and (and (and (= x_28 3) ?v_118) ?v_115) ?v_116) (= x_31 x_17)) ?v_119))) (= x_13 (+ x_6 1))) (= x_457 (select x_2 x_15))) (= x_458 (select x_2 x_18))) (= x_459 (select x_2 x_20))) (or (or (or (and (and (and (and (and (and (and (= x_14 0) (= x_12 (+ x_1 1))) ?v_120) ?v_121) (= x_16 x_15)) (= x_457 1)) (= x_17 (store x_2 x_15 2))) (= x_9 (store x_7 x_1 x_15))) (and (and (and (and (and (and (and (and (and (= x_14 1) ?v_122) ?v_120) ?v_121) ?v_123) ?v_124) (= x_19 x_18)) (= x_458 2)) (= x_8 x_18)) (= x_17 (store x_2 x_18 3)))) (and (and (and (and (and (and (and (and (and (= x_14 2) ?v_122) (= x_10 (+ x_0 1))) ?v_121) ?v_123) ?v_124) (= x_21 x_20)) (= x_459 3)) (or (not (<= x_6 12)) (= x_8 x_20))) (= x_17 (store x_2 x_20 1)))) (and (and (and (and (and (= x_14 3) ?v_123) ?v_120) ?v_121) (= x_17 x_2)) ?v_124))) (= x_460 (select x_353 x_3))) (= x_461 (select x_353 x_4))) (= x_462 (select x_339 x_3))) (= x_463 (select x_339 x_4))) (= x_464 (select x_325 x_3))) (= x_465 (select x_325 x_4))) (= x_466 (select x_311 x_3))) (= x_467 (select x_311 x_4))) (= x_468 (select x_297 x_3))) (= x_469 (select x_297 x_4))) (= x_470 (select x_283 x_3))) (= x_471 (select x_283 x_4))) (= x_472 (select x_269 x_3))) (= x_473 (select x_269 x_4))) (= x_474 (select x_255 x_3))) (= x_475 (select x_255 x_4))) (= x_476 (select x_241 x_3))) (= x_477 (select x_241 x_4))) (= x_478 (select x_227 x_3))) (= x_479 (select x_227 x_4))) (= x_480 (select x_213 x_3))) (= x_481 (select x_213 x_4))) (= x_482 (select x_199 x_3))) (= x_483 (select x_199 x_4))) (= x_484 (select x_185 x_3))) (= x_485 (select x_185 x_4))) (= x_486 (select x_171 x_3))) (= x_487 (select x_171 x_4))) (= x_488 (select x_157 x_3))) (= x_489 (select x_157 x_4))) (= x_490 (select x_143 x_3))) (= x_491 (select x_143 x_4))) (= x_492 (select x_129 x_3))) (= x_493 (select x_129 x_4))) (= x_494 (select x_115 x_3))) (= x_495 (select x_115 x_4))) (= x_496 (select x_101 x_3))) (= x_497 (select x_101 x_4))) (= x_498 (select x_87 x_3))) (= x_499 (select x_87 x_4))) (= x_500 (select x_73 x_3))) (= x_501 (select x_73 x_4))) (= x_502 (select x_59 x_3))) (= x_503 (select x_59 x_4))) (= x_504 (select x_45 x_3))) (= x_505 (select x_45 x_4))) (= x_506 (select x_31 x_3))) (= x_507 (select x_31 x_4))) (= x_508 (select x_17 x_3))) (= x_509 (select x_17 x_4))) (= x_510 ?v_125)) (= x_511 ?v_126)) (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (and (= x_460 3) (= x_461 3)) (and (= x_462 3) (= x_463 3))) (and (= x_464 3) (= x_465 3))) (and (= x_466 3) (= x_467 3))) (and (= x_468 3) (= x_469 3))) (and (= x_470 3) (= x_471 3))) (and (= x_472 3) (= x_473 3))) (and (= x_474 3) (= x_475 3))) (and (= x_476 3) (= x_477 3))) (and (= x_478 3) (= x_479 3))) (and (= x_480 3) (= x_481 3))) (and (= x_482 3) (= x_483 3))) (and (= x_484 3) (= x_485 3))) (and (= x_486 3) (= x_487 3))) (and (= x_488 3) (= x_489 3))) (and (= x_490 3) (= x_491 3))) (and (= x_492 3) (= x_493 3))) (and (= x_494 3) (= x_495 3))) (and (= x_496 3) (= x_497 3))) (and (= x_498 3) (= x_499 3))) (and (= x_500 3) (= x_501 3))) (and (= x_502 3) (= x_503 3))) (and (= x_504 3) (= x_505 3))) (and (= x_506 3) (= x_507 3))) (and (= x_508 3) (= x_509 3))) (and (= x_510 3) (= x_511 3))))))
(check-sat)
(exit)
